Главная arrow книги arrow Копия Глава 9. Логический вывод в логике первого п arrow Эффективный прямой логический вывод
Эффективный прямой логический вывод

•    Можно приложить определенные усилия по устранению излишних попыток согласования с правилами в алгоритме прямого логического вывода, что является темой следующего раздела.

Инкрементный прямой логический вывод

Когда авторы демонстрировали в предыдущем разделе на примере доказательства преступления, как действует прямой логический вывод, они немного схитрили; в частности, не показали некоторые из согласований с правилами, выполняемые алгоритмом, приведенным в листинге 9.2. Например, во второй итерации правило согласуется с фактом(еще раз), и, безусловно, при этом ничего не происходит, поскольку заключениеуже известно. Таких излишних согласований с правилами можно избежать, сделав следующее наблюдение: каждый новый факт, выведенный в итерации t, долэ/сен быть получен по меньшей мере из одного нового факта, выведенного в итерации t-Ι. Это наблюдение соответствует истине, поскольку любой логический вывод, который не требовал нового факта из итерации t-1, уже мог быть выполнен в итерации t-1.

Такое наблюдение приводит естественным образом к созданию алгоритма инкре-ментного прямого логического вывода, в котором в итерации t проверка правила происходит, только если его предпосылка включает конъюнкт pi, который унифицируется с фактом, вновь выведенным в итерации t-1. Затем на этапе согласования с правилом значениефиксируется для согласования с, но при этом допускается, чтобы остальные конъюнкты в правиле согласовывались с фактами из любой предыдущей итерации. Этот алгоритм в каждой итерации вырабатывает точно такие же факты, как и алгоритм, приведенный в листинге 9.2, но является гораздо более эффективным.

При использовании подходящей индексации можно легко выявить все правила, которые могут быть активизированы любым конкретным фактом. И действительно, многие реальные системы действуют в режиме "обновления", при котором прямой логический вывод происходит в ответ на каждый новый факт, сообщенный системе с помощью операции Tell. Операции логического вывода каскадно распространяются через множество правил до тех пор, пока не достигается фиксированная точка, а затем процесс начинается снова, вслед за поступлением каждого нового факта.